(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix Transpose *)
Require Import List.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.list_function.
Require Import Matrix.Mat.Mat_IO.
Require Import Matrix.Mat.Mat_map.


(* ################################################################# *)
(** * Definition of Matrix Transpose *)

Section Mat_trans.

Variable A:Set.
Variable Zero:A.

(** ** Two-dimensional List Transformation Processing Functions *)

(** These functions are to help achieve matrix transposition. *)

(** *** headcolumn *)
(** Get the first column of the two-dimensional list. *)
Fixpoint headcolumn (m:list (list A)) :=
  match m with
  | nil => nil
  | cons x x' => (@hd A Zero x)::(headcolumn x')
  end.

(** *** tailcolumn *)
(** Get the rest part of the two-dimensional table except the first
    column of elements. *)
Fixpoint tailcolumn (m:list(list A )) :=
  match m with
  | nil => nil
  | cons x x' => (tl x)::(tailcolumn x')
  end.

(** *** gettrans *)
(** Transpose the two-dimensional list of width n. *)
Fixpoint gettrans(m:list (list A)) (n:nat):=
  match n with
  | O => nil_list A n
  | S n' => (headcolumn m)::(gettrans (tailcolumn m) n')
  end.

(** *** link *)
(** Connect a list to the left side of the matrix. *)
Fixpoint link (l:list A)(m:list (list A)):=
  match l ,m with
  | cons x x' ,cons y y' => (x::y) :: (link x' y')
  | _,_ => nil
  end.



(** ** Properties of Functions Above *)

Section dlist_lemma.

(** *** head_same *)
(** List a is equal to the connection of its head and its tail. *)
Lemma hd_same : forall (a:list A) n,
  length a = n -> n<>0 -> @hd A Zero a :: tl  a = a.
Proof.
  induction a.
  simpl. intros. rewrite H in H0. destruct H0. auto. simpl. intros. auto.
Qed.

(** *** link_head_tail *)
Lemma link_head_tail : forall (ma:list (list A)) n,
  n <> 0 ->width ma n ->
  ma = link (headcolumn ma) (tailcolumn ma).
Proof.
  induction ma.
  - induction n.
    * intros. simpl. auto.
    * simpl. auto.
  - induction n.
    * intros. destruct H. auto.
    * intros. simpl. rewrite hd_same with (n:= S n).
      f_equal. apply IHma with (n:= S n).
      apply H. inversion H0. apply H2. inversion H0. apply H1.
      apply H.
Qed.

(** *** length_headcolumn *)
(** The length of the first column of a two-dimensional list
    with width n is n. *)
Lemma length_headcolumn : forall (m:list(list A)) (n:nat) ,
   height m = n -> length (headcolumn m) = n.
Proof.
  induction m.
  - simpl. auto.
  - simpl. intros. induction n. inversion H. rewrite IHm with(n:=n).
     auto. auto.
Qed.

(** *** height_gettrans *)
(** The width of a two-dimensional list with width n remain the same
    after transposition. *)
Lemma height_gettrans: forall (n:nat) (ma:list(list A)),
  height (gettrans ma n) = n.
Proof.
  induction n.
  - simpl. auto.
  - simpl. intros. f_equal. rewrite IHn. auto.
Qed.

(** *** all_len_In *)
(** If list l is one list of the  two-dimensional list ma and l has
    length n, then the width of ma is n. *)
Lemma width_In : forall (ma:list (list A)) (n:nat),
 (forall l ,In l ma -> length l = n) -> width ma n.
Proof.
  induction ma.
  - simpl. auto.
  - induction n. simpl. intros. split. apply H. left. auto.
    apply IHma. intros. apply H. right. auto. simpl. intros. 
    split. apply H. auto. apply IHma. intros. apply H. auto.
Qed.

(** *** height_tailcolumn *)
(** If the height of the two-dimensional list ma is m, the height of the
    rest part of ma excluding the first column is still m. *)
Lemma height_tailcolumn : forall(ma:list (list A)) m,
  height ma = m -> 
  height ( tailcolumn ma ) = m.
Proof.
  induction ma.
  - simpl. auto.
  - simpl. intros. rewrite IHma with (m:=pred m). 
    rewrite <- H. simpl. auto. rewrite <- H. simpl. auto.
Qed.

(** *** width_gettrans *)
(** After transposing the two-dimensional list with the
    number of rows m, the number of columns is m. *)
Lemma width_gettrans : forall m n (ma:list(list A)), 
    height ma = m ->
    width (gettrans ma n) m.
Proof.
  induction n.
  - intros. unfold gettrans. simpl. auto.
  - intros. unfold gettrans. unfold width. simpl.
    split. apply length_headcolumn. apply H.
    apply IHn. apply height_tailcolumn. auto.
Qed.

(** *** dlist_link *)
(** The two-dimensional list ma is equal to the connection of its first
    column and the rest two-dimensional list. *)
Lemma dlist_link : forall (n:nat) (ma:list(list A)), 
  n <> 0 -> width ma n -> ma = link (headcolumn ma) (tailcolumn ma).
Proof.
  induction ma.
  - intros. simpl. auto.
  - intros. simpl. rewrite hd_same with (n:=n).
    f_equal. apply IHma. apply H. inversion H0. apply H2. inversion H0.
    apply H1. apply H.
Qed.

End dlist_lemma.

(** ** trans *)
(** Transpose the matrix and return : T(A). *)
Definition trans {m n:nat} (ma:@Mat A m n):(@Mat A n m ):=
  let cond1 := height_gettrans n (mat A m n ma) in
  let cond2 := width_gettrans m n (mat A m n ma)
               (mat_height A m n  ma ) in
  mkMat A n m (gettrans (mat A m n ma) n) cond1 cond2.

End Mat_trans.

Section lemma.
Variable A:Set.
Variable Zero:A.
Variable add: A->A->A.

(** *** length_tl *)
(** If the length of table l is n, the length of tail l is n-1. *)
Lemma length_tl:forall n (a:list A),
  length a = S n -> length(tl a) = n.
Proof.
  induction n. induction a. simpl. auto.
  intros. simpl. inversion H. auto.
  induction a. intros. inversion H. intros. 
  simpl. inversion H. auto.
Qed.


(** *** mat_each'_nil_list *)
Lemma mat_each'_nil_list : forall(n:nat),
  mat_each' A add (nil_list A n )(nil_list A n ) = (nil_list A n ).
Proof.
  induction n.
  - simpl. auto.
  - simpl. f_equal. apply IHn. 
Qed.

Lemma hd_list_each : forall m (l1 l2:list A),
  length l1 = m -> length l2 = m ->
  (forall a , add a Zero = a) ->
  @hd A Zero (list_each A add l1 l2) = 
  add (@hd A Zero l1) (@hd A Zero l2).
Proof.
  induction m.
  - induction l1.
    + induction l2.
      * intros. simpl. rewrite H1. auto.
      * intros. inversion H0.
    + intros. inversion H.
  - induction l1.
    + intros. inversion H.
    + induction l2. 
      * intros. inversion H0.
      * intros. simpl. auto.
Qed.

Lemma headcolumn_mat_each': forall m n(ma mb:list(list A)),
  height ma = m -> height mb = m ->
  width ma n -> width mb n ->
   (forall a , add a Zero = a) ->
  headcolumn A Zero (mat_each' A add ma mb) = 
  list_each A add (headcolumn A Zero ma) (headcolumn A Zero mb).
Proof.
  induction m.
  - induction n.
    + induction ma.
      * induction mb.
        intros. simpl. auto. intros. inversion H0.
      * intros. inversion H.
    + induction ma. 
      * induction mb.
        intros. simpl. auto. intros. inversion H0.
      * intros. inversion H.
  - induction n.
    + induction ma.
      * intros. inversion H.
      * induction mb.
        intros. inversion H0. intros. simpl. 
        rewrite hd_list_each with(m:=0).
        f_equal. apply IHm with (n:=0).
        inversion H. auto. inversion H0. auto.
        inversion H1. apply H5. inversion H2. apply H5.
        apply H3. inversion H1. apply H4. inversion H2. apply H4.
        apply H3.
    + induction ma.
      * intros. inversion H.
      * induction mb.
        intros. inversion H0. intros. simpl. 
        rewrite hd_list_each with(m:=S n).
        f_equal. apply IHm with (n:=S n).
        inversion H. auto. inversion H0. auto.
        inversion H1. apply H5. inversion H2. apply H5.
        apply H3. inversion H1. apply H4. inversion H2.
        apply H4. apply H3.
Qed.

Lemma tl_list_each:forall n l1 l2,
  length l1 = n -> length l2 = n ->
  tl (list_each A add l1 l2 ) =
  list_each A add (tl l1) (tl l2).
Proof.
  induction n.
  - induction l1.
    + induction l2.
      * auto. * intros. inversion H0.
    + intros. inversion H.
  - induction l1.
    + intros. inversion H.
    + induction l2.
      * intros. inversion H0. * intros. simpl. auto.
Qed.

Lemma tailcolumn_mat_each': forall m n ma mb,
  height ma = m -> height mb = m ->
    width ma n -> width mb n->
  tailcolumn A (mat_each' A add ma mb) =
  mat_each' A add (tailcolumn A ma) (tailcolumn A mb).
Proof.
  induction m.
  - induction n.
    + induction ma.
      * induction mb. intros. auto. intros. inversion H0.
      * intros. inversion H.
    + induction ma. 
      * induction mb. intros. auto. intros. inversion H0.
      * intros. inversion H.
  - induction n.
    + induction ma. 
      * intros. inversion H.
      * induction mb. intros. inversion H0. intros.
        simpl. rewrite tl_list_each with (n:= 0).
        f_equal. apply IHm with (n:=0). inversion H.
        auto. inversion H0. auto. inversion H1. apply H4.
        inversion H2. apply H4. inversion H1. apply H3.
        inversion H2. apply H3.
    + induction ma.
      * intros. inversion H.
      * induction mb. intros. inversion H0.
        intros. simpl. rewrite tl_list_each with (n:= S n).
        f_equal. apply IHm with (n:=S n). inversion H.
        auto. inversion H0. auto. inversion H1. apply H4.
        inversion H2. apply H4. inversion H1. apply H3.
        inversion H2. apply H3.
Qed. 


Lemma width_tailcolumn: forall n ma,
  width ma (S n) ->
  width (tailcolumn A ma) n.
Proof.
  induction n.
  - induction ma.
    + intros. simpl. apply I.
    + intros. simpl. inversion H. rewrite length_tl with(n:=0).
      split. auto. apply IHma. apply H1. apply H0.
  - induction ma.
    + intros. simpl. apply I.
    + intros. simpl. rewrite length_tl with(n:=(S n)).
      split. auto. apply IHma. inversion H. apply H1. inversion H. apply H0.
Qed.

Lemma pred_S: forall n,
  pred(S n) = n.
Proof. induction n.
  - simpl. auto. - simpl. auto.
Qed.

(** *** gettrans_nil *)
(** gettrans nil n equals to nil_list n. *)
Lemma gettrans_nil :forall n,
  gettrans A Zero nil n = nil_list A n.
Proof.
  induction n.
  - simpl. reflexivity. 
  - simpl. f_equal. apply IHn.
Qed.

(** *** gettrans_mat_each' *)
Lemma gettrans_mat_each': forall(m n:nat) (ma mb:list (list A)),
  height ma = m -> height mb = m ->
  width ma n -> width mb n->
  (forall a , add a Zero = a) ->
  gettrans A Zero (mat_each' A add ma mb) n 
  = mat_each' A add (gettrans A Zero ma n)(gettrans A Zero mb n).
Proof.
  induction m.
  - induction n.
    + induction ma.
      * simpl. auto.
      * simpl. auto.
    + induction ma.
      * intros. simpl. f_equal.
        rewrite ?gettrans_nil with(n0:=n). 
        induction mb.
        { simpl. rewrite ?gettrans_nil with(n:=n).
          rewrite mat_each'_nil_list.
          reflexivity. }
        { simpl. inversion H0. }
      * intros. inversion H.
  - induction n.
    + simpl. auto.
    + induction ma. 
      * intros. inversion H.
      * induction mb. intros. inversion H0.
        intros. simpl. rewrite hd_list_each with(m:= S n).
        f_equal. f_equal. 
        rewrite headcolumn_mat_each' with (m:=m) (n:=S n).
        f_equal. inversion H. auto. inversion H0. auto.
        inversion H1. apply H5. inversion H2. apply H5.
        apply H3. rewrite <-IHn. f_equal. 
        rewrite tl_list_each with (n:=S n).
        simpl. f_equal. rewrite tailcolumn_mat_each' with(m:= m)(n:=S n).
        f_equal. inversion H. auto. inversion H0. auto. inversion H1. 
        apply H5. inversion H2. apply H5. inversion H1. apply H4.
        inversion H2. apply H4. simpl. rewrite height_tailcolumn with (m:= m).
        auto. inversion H. auto. simpl. rewrite height_tailcolumn with (m:= m).
        auto. inversion H0. auto.  simpl. inversion H1. 
        rewrite length_tl with (n:= n). split. auto. rewrite <- pred_S .
        apply width_tailcolumn. apply H5. apply H4. simpl.
        rewrite length_tl with (n:= n). split. auto. rewrite <- pred_S .
        apply width_tailcolumn. inversion H2. apply H5. inversion H2. apply H4.
        apply H3. inversion H1. apply H4. inversion H2. apply H4. apply H3.
Qed.

(** *** gettrans_nil' *)
(** gettrans nil m to get a two-dimensional table with zero columns
    and m rows. *)
Lemma gettrans_nil' : forall m (ma:list(list A)),
  height ma = m -> width ma 0 -> 
  gettrans A Zero nil m = ma.
Proof.
  induction m.
  - simpl. intros. unfold height in H. rewrite length_zero_iff_nil in H.
     rewrite H. auto.
  - simpl. induction ma. simpl. intros. inversion H. 
    simpl. intros. rewrite IHm with (ma:=ma). destruct H0.
    rewrite length_zero_iff_nil in H0. rewrite H0. auto. auto. 
    apply H0.
Qed.

(** *** all_In' *)
(** If the number of columns in the two-dimensional table ma is S n,
    the number of columns in tailcolumn ma is n. *)
Lemma width_In':forall n (ma:list (list A)),
  width ma (S n) -> width (tailcolumn A ma ) n.
Proof.
  intros n ma. generalize dependent n.
  induction ma.
  - intros. induction n.
    + simpl. apply I.
    + simpl. apply I.
  - induction n.
    + simpl . intros. split.
      { destruct H as [H1 H2]. apply length_tl in H1. rewrite H1. auto. }
      { destruct H as [H1 H2]. apply IHma. apply H2. }
    + intros. induction n.
      { simpl. split. 
        { simpl in H. destruct H as [H1 H2]. apply length_tl in H1.
          rewrite H1. auto. }
        { simpl in H. destruct H as [H1 H2]. apply IHma. apply H2. }
      }
      { simpl. split.
        { simpl in H. destruct H as [H1 H2]. apply length_tl in H1.
          rewrite H1. auto. }
        { simpl in H . destruct H as [H1 H2]. apply IHma. apply H2. }
      }
Qed.

(** *** link_gettrans *)
(** The relationship between link and gettrans function. *)
Lemma link_gettrans : forall m n l (ma:list (list A)),
  length l = n -> height ma = m ->width ma n -> 
  link A l (gettrans A Zero ma n) = gettrans A Zero (l::ma) n.
Proof.
  intros m n. generalize dependent m.
  induction n.
  - intros. simpl. induction l. 
    + simpl. auto. + inversion H.
  - intros. simpl. induction l.
    + simpl in H0. discriminate H.
    + simpl. f_equal. apply IHn with m. inversion H. auto.
      apply height_tailcolumn. apply H0. apply width_In' in H1.
      apply H1.
Qed.

(** *** link_charge *)
(** Link function and the relationship between head and tail function. *)
Lemma link_charge: forall l l2 (ma:list(list A)) m,
  length l = S m -> 
  link A l (l2::ma) = (@hd A Zero l :: l2):: (link A (tl  l) ma).
Proof.
  induction l.
  - simpl. intros. inversion H.
  - simpl. intros. auto.
Qed.

(** *** headcolumn_link *)
(** The relationship between headcolumn and link. *)
Lemma headcolumn_link : forall a ma m, 
  length a = m -> height ma = m -> 
  headcolumn A Zero (link A a ma) = a.
Proof.
  induction a.
  - simpl. auto. 
  - induction ma.
    + simpl. intros. rewrite <- H in H0. inversion H0. 
    + intros. 
      assert(link A (a :: a0) (a1 :: ma) = (a::a1)::(link A a0 ma)). 
      simpl. auto. rewrite H1. simpl. rewrite IHa with (m:=pred m).
      auto. simpl in H. rewrite <- H. simpl. auto. rewrite <- H0.
      simpl. auto.
Qed.

(** *** tail_column_link *)
(** The relationship between tailcolumn and link. *)
Lemma tailcolumn_link : forall a (ma:list (list A)) m, 
    length a = m -> height ma = m -> 
    tailcolumn A (link A a ma) = ma.
Proof.
  induction a.
  - simpl. intros. rewrite <- H in H0. induction ma. auto. 
    inversion H0.
  - induction ma.
    + intros. simpl in H0. rewrite <- H0 in H. inversion H.
    + simpl. intros. rewrite IHa with (m:=pred m). auto.
      rewrite <- H. auto. rewrite <- H0. auto.
Qed.

(** *** gettrans_link *)
(** The relationship between gettrans and link. *)
Lemma gettrans_link : forall a ma m n,
  length a = n -> height ma =n -> 
  gettrans A Zero (link A a ma) (S m) = a :: gettrans A Zero ma m.
Proof.
  intros.
  induction m.
  - simpl. rewrite headcolumn_link with (m:=n);auto.
  - unfold gettrans. rewrite headcolumn_link with (m:=n). 
    f_equal. rewrite tailcolumn_link with (m:=n). 
    auto. auto. auto. auto. auto.
Qed.

(** *** trans_same *)
(** Two-dimensional list is equal to itself after two gettrans
    operations. *)
Lemma trans_same : forall ma m n , 
    height ma = m-> width ma n  ->
    gettrans A Zero (gettrans A Zero ma n) m = ma.
Proof.
induction ma as [|x' mma' IHma'].
- simpl. intros. rewrite <- H. simpl. auto.
- induction m as [|m' IHm']. 
  + simpl. intros. inversion H.
  + simpl. intros. destruct H0.
    induction n as [|n' IHn'].
      { simpl. rewrite length_zero_iff_nil in H0. rewrite H0. f_equal.
        apply gettrans_nil'. auto. auto. }
      { intros. rewrite <- link_gettrans with (m:=m').
       rewrite headcolumn_link with (m:=S n').
       rewrite tailcolumn_link with (m:=S n').
       rewrite IHma'. simpl. f_equal.
       inversion H. auto. apply H1.
        inversion H0. auto.
        apply height_gettrans.
        apply H0. apply height_gettrans. apply H0. inversion H. auto.
        apply H1.
      } 
Qed.

Lemma headcolumn_nil_list: forall m,
  headcolumn A Zero (nil_list A m) = list_o A Zero m.
Proof.
  induction m. simpl. auto.
  simpl. f_equal. apply IHm.
Qed.

Lemma headcolumn_gettrans: forall m n ma,
  length ma = m -> width ma n ->
  headcolumn A Zero (gettrans A Zero ma n) 
  = @hd (list A) (list_o A Zero n) ma.
Proof.
  induction m . intros. apply length_zero_iff_nil in H.
  rewrite H. rewrite gettrans_nil. simpl. apply headcolumn_nil_list.
  induction n. intros. unfold head. simpl. 
  apply width_dlist_0 with(m:= S m)in H0 .
  rewrite H0. simpl. auto. apply H.
  induction ma. intros. inversion H. intros.
  simpl. rewrite IHn. rewrite hd_same with(n:=S n).
  auto. apply H0. auto. simpl. f_equal. apply height_tailcolumn.
  inversion H. auto. simpl. split. apply length_tl.
  apply H0. apply width_tailcolumn. apply H0.
Qed.

Lemma tailcolumn_nil_list: forall m,
  tailcolumn A (nil_list A m) = nil_list A m.
Proof.
  induction m. simpl. auto.
  simpl. f_equal. apply IHm.
Qed.
  
Lemma tailcolumn_gettrans:forall m n (ma:list(list A)),
  height ma = m -> width ma n ->
  tailcolumn A (gettrans A Zero ma n)
  = gettrans A Zero (tl ma) n .
Proof.
  induction m. intros. apply length_zero_iff_nil in H.
  rewrite H. simpl. rewrite gettrans_nil.
  rewrite tailcolumn_nil_list. auto.
  induction n. simpl. auto. induction ma.
  intros. inversion H. intros. simpl.
  f_equal. apply IHn. simpl. f_equal. apply height_tailcolumn.
  inversion H. auto. simpl. split. apply length_tl.
  apply H0. apply width_tailcolumn. apply H0.
Qed.



End lemma.

Section Mat_link.

Variable A:Set.
Variable Zero:A.

Lemma height_link :forall h (a:list A)(ma:list (list A)),
  length a = h -> height ma = h ->
  height (link A a ma) = h.
Proof.
  induction h.
  induction a.
  intros. simpl. auto. intros. inversion H.
  induction a. intros. inversion H.
  induction ma. intros. inversion H0.
  intros. simpl. f_equal. apply IHh.
  inversion H. auto. inversion H0. auto.
Qed.


Lemma width_link: forall h w(a:list A)(ma:list (list A)),
  length a = h -> height ma =  h-> width ma w->
  width( link A a ma) (S w).
Proof.
  induction h. induction a. simpl. auto.
  intros. inversion H. 
  induction a. intros. inversion H.
  induction ma. intros. inversion H0. intros. simpl.
  split. f_equal. apply H1. apply IHh. inversion H.
  auto. inversion H0. auto. apply H1.
Qed.

(* Definition mlink(ma mb:list (list A)) m n p:list (list A):=
  let ma' :=gettrans A Zero ma n in
  let mb' :=gettrans A Zero mb p in
    gettrans A Zero (app ma' mb') m. *)

(* n为ma列数 横向合并ma mb*)
(* Fixpoint mlink' ma mb n:=
  match n with
  | O => mb
  | S n' => link A (headcolumn A Zero ma)
            (mlink' (tailcolumn A ma) mb n')
  end. *)

Fixpoint mlink (ma mb:list (list A)):=
  match ma with
  | nil => mb
  | x::x' => match mb with
             | nil => ma
             | y::y' => (x++y):: (mlink x' y')
             end
  end.

Lemma height_mlink:forall m ma mb,
  height ma = m -> height mb = m ->
  height (mlink ma mb) = m.
Proof.
  induction m.
  induction ma. intros. simpl. auto.
  intros. inversion H.
  induction ma. intros. inversion H.
  induction mb. intros. inversion H0.
  intros. simpl. f_equal. apply IHm.
  inversion H. auto. inversion H0. auto.
Qed.

Lemma width_mlink:forall m w1 w2 ma mb,
  height ma = m -> height mb = m ->
  width ma w1 -> width mb w2 ->
  width (mlink ma mb) (w1+w2).
Proof.
  induction m. intros. apply length_zero_iff_nil in H.
  apply length_zero_iff_nil in H0. rewrite H,H0.
  simpl. auto.
  induction ma. intros. inversion H. induction mb.
  intros. inversion H0. intros.
  simpl. split. apply length_app. apply H1. apply H2.
  apply IHm. inversion H. auto. inversion H0. auto.
  apply H1. apply H2.
Qed. 

Lemma height_app:forall m1 m2 (ma mb:list(list A)),
  height ma = m1 ->height mb = m2->
  height(ma++mb) = m1 + m2.
Proof.
  induction m1.
  induction m2.
  induction ma. induction mb. auto. intros. inversion H0.
  intros. inversion H. induction ma. induction mb.
  intros. inversion H0. intros. simpl. f_equal. inversion H0.
  auto. induction mb. intros. inversion H0.
  intros. inversion H.
  induction m2.
  induction ma. induction mb. intros. inversion H.
  intros. inversion H0. induction mb.
  intros. simpl. f_equal. apply IHm1. inversion H. auto. auto.
  intros. inversion H0. induction ma. intros. inversion H.
  induction mb. intros. inversion H0. intros. simpl.
  f_equal. apply IHm1. inversion H. auto. apply H0.
Qed.

Variable f:A->A->A.

(** The relationship between list_each and app *)
Lemma list_each_app: forall m n a a0 a1 a2,
  length a = m-> length a1 = m ->
  length a0 = n -> length a2 = n ->
  list_each A f (a ++ a0) (a1 ++ a2) =
  (list_each A f a a1 ++ list_each A f a0 a2).
Proof.
  induction m. - induction a. + induction a1.
  simpl. auto. intros. inversion H0.
  + intros. inversion H.
  - induction n. + induction a0. * induction a2.
    simpl. rewrite ?app_nil_r. auto.
    intros. inversion H2. * intros. inversion H1.
    + induction a. intros. inversion H.
      induction a2. intros. inversion H0.
      induction a1. intros. inversion H1.
      induction a5. intros. inversion H2.
      intros. simpl. f_equal. apply IHm with(n:=S n).
      inversion H. auto. inversion H0. auto.
      auto. auto.
Qed.

Lemma mat_each'_mlink: forall m n p ma mb mc md,
  (forall a, f a Zero = a)->
  height ma = m->height mb = m ->height mc = m
  ->height md = m ->width ma  n->width mb  p
  -> width mc  n -> width md  p->
  mat_each' A f (mlink ma mb ) (mlink mc md )
  = mlink(mat_each' A f ma mc) (mat_each' A f mb md).
Proof.
  induction m.
  - induction ma.
    + induction mc. simpl. auto.
      intros. inversion H2.
    + intros. inversion H0.
  - induction ma.
    intros.
    inversion H0.
    induction mb. intros. inversion H1. induction mc.
    intros. inversion H2. induction md. intros. 
    inversion H3. intros. simpl. 
    rewrite list_each_app with(m:=n)(n:=p).
    f_equal. apply IHm with(n:=n)(p:=p).
    auto. inversion H0. auto. inversion H1. auto.
    inversion H2. auto. inversion H3. auto.
    apply H4. apply H5. apply H6. apply H7.
    apply H4. apply H6. apply H5. apply H7.
Qed.

Lemma dlist_map_mlink: forall f1 h a b,
  height a = h -> height b = h ->
  dlist_map A f1 (mlink a b) 
  = mlink (dlist_map A f1 a) (dlist_map A f1 b).
Proof.
  induction h. 
  - induction a. simpl. auto. intros. inversion H.
  - induction a. intros. inversion H.
    induction b. intros. inversion H0.
    intros. simpl. f_equal. apply list_map_app.
    apply IHh. inversion H. auto. inversion H0.
    auto.
Qed.
 
Lemma mlink_nil_list_l: forall m (ma:list (list A)),
  height ma = m -> 
  mlink (nil_list A m) ma = ma.
Proof.
  induction m.
  induction ma. simpl. auto.
  intros. inversion H.
  induction ma. intros. inversion H.
  intros. simpl. f_equal. apply IHm. inversion H. auto.
Qed.

Lemma mlink_nil_list_r: forall m (ma:list (list A)),
  height ma = m -> 
  mlink ma (nil_list A m) = ma.
Proof.
  induction m.
  induction ma. simpl. auto.
  intros. inversion H.
  induction ma. intros. inversion H.
  intros. simpl. rewrite app_nil_r.
  f_equal. apply IHm. inversion H. auto.
Qed.

End Mat_link. 

Section column_n.

Variable A:Set.
Variable Zero:A.
Fixpoint head_n (ma:list A) n:=
  match n with
  | O => nil
  | S n' => (@hd A Zero ma)::(head_n (tl ma) n')
  end.

Lemma length_head_n : forall ma w,
  length(@head_n ma w) = w.
Proof.
  induction ma. induction w. simpl. auto.
  simpl. f_equal. apply IHw.
  induction w. simpl. auto. simpl.
  f_equal. apply IHma.
Qed.

Fixpoint headcolumn_n (ma:list(list A)) n:=
  match ma with
  | nil => nil
  | x::x' => (head_n x n)::(headcolumn_n x' n)
  end.

Lemma height_headcolumn_n : forall h w ma,
  height ma = h -> 
  height(headcolumn_n ma w) = h.
Proof.
  induction h. induction ma. auto.
  intros. inversion H. induction ma.
  intros. inversion H. intros. simpl.
  f_equal. apply IHh. inversion H. auto.
Qed.

Lemma width_headcolumn_n: forall w ma,
  width(headcolumn_n ma w) w.
Proof.
  induction w. induction ma. simpl. auto.
  simpl. split. auto. auto.
  induction ma. simpl. auto. simpl. split.
  f_equal. apply length_head_n. apply IHma.
Qed.

Fixpoint tail_n (ma:list A) n:=
  match n with
  | O => ma
  | S n' => tail_n( tl ma )n' 
  end.

Lemma length_tail_n : forall w1 w2 ma,
  length ma = w1+w2 ->
  length (tail_n ma w1) =w2.
Proof.
  induction w1. induction w2. simpl. auto.
  induction ma. intros. inversion H. intros. simpl.
  f_equal. inversion H. auto.
  induction w2. intros. simpl. apply IHw1. apply length_tl.
  rewrite H. auto. induction ma.
  intros. inversion H. intros. simpl. apply IHw1.
  inversion H. auto.
Qed.

Fixpoint tailcolumn_n (ma:list(list A)) n:=
  match ma with
  | nil => nil
  | x::x' => (tail_n x n) ::(tailcolumn_n x' n)
  end.

Lemma height_tailcolumn_n: forall h w ma,
  height ma = h->
  height(tailcolumn_n ma w) = h.
Proof.
  induction h. - induction w.
  + induction ma. simpl. auto. intros. inversion H.
  + induction ma. simpl. auto. intros. inversion H.
  - induction w. + induction ma. intros. inversion H.
  intros. simpl. f_equal. apply IHh. inversion H. auto. 
  + induction ma. intros. inversion H.
    intros. simpl. f_equal. apply IHh. inversion H.
    auto.
Qed.

Lemma width_tailcolumn_n: forall w1 w2 ma,
  width ma (w1+w2) ->
  width(tailcolumn_n ma w1)(w2).
Proof.
  induction w1. induction w2. 
  induction ma. simpl. auto. intros. simpl. split.
  apply H. apply IHma. apply H.
  induction ma. intros. simpl. auto. intros.
  simpl. split. apply H. apply IHma. apply H.
  induction w2. induction ma. simpl. auto.
  intros. simpl. split. apply length_tail_n.
  apply length_tl. apply H. apply IHma. apply H.
  induction ma. simpl. auto. intros. simpl.
  split. apply length_tail_n. apply length_tl.
  apply H. apply IHma. apply H.
Qed.

Lemma headcolumn_app: forall ma mb,
  headcolumn A Zero (ma++ mb) = (headcolumn A Zero ma)++(headcolumn A Zero mb).
Proof.
  induction ma. induction mb. simpl. auto.
  simpl. auto. induction mb. simpl. rewrite ?app_nil_r. auto. 
  simpl. f_equal. apply IHma.
Qed.

Lemma tailcolumn_app: forall ma mb,
  tailcolumn A (ma ++ mb) = (tailcolumn A ma)++(tailcolumn A mb).
Proof.
  induction ma. simpl. auto.
  induction mb. intros. simpl. f_equal. rewrite ?app_nil_r.
  auto. intros. simpl. f_equal. apply IHma. 
Qed.

Lemma head_n_tail: forall a w,
  length a = S w ->
  @hd A Zero a :: head_n (tl a) w = a.
Proof.
  induction a. intros. inversion H. induction w.
  intros. inversion H. apply length_zero_iff_nil in H1.
  rewrite H1. simpl. auto.
  intros. simpl. f_equal. apply IHa. inversion H. auto.
Qed.

Lemma head_n_nil: forall w,
  head_n nil w = list_o A Zero w.
Proof.
  induction w.
  simpl. auto. simpl. f_equal.
  apply IHw.
Qed.

Lemma headcolumn_n_0: forall w ma,
  length ma = w ->
  headcolumn_n ma 0 = nil_list A w.
Proof.
  induction w. induction ma. simpl. auto.
  intros. inversion H. induction ma.
  intros. inversion H. intros. simpl.
  f_equal. apply IHw. inversion H. auto.
Qed.

Lemma head_n_app_n:forall w a b,
  length a = w ->
  head_n(a++b) w = a.
Proof.
  induction w. - simpl. intros. apply length_zero_iff_nil in H. 
  rewrite H. auto. 
  - induction a. intros. inversion H. 
    intros. simpl. f_equal. apply IHw. inversion H. auto.
Qed.

Lemma headcolumn_n_mlink: forall h n ma mb,
  height ma = h -> height mb = h ->
  width ma n ->
  headcolumn_n (mlink A ma mb) n = ma.
Proof.
  induction h. - intros. apply length_zero_iff_nil in H.
  apply length_zero_iff_nil in H0. rewrite H,H0. simpl. auto.
  - induction ma. intros. inversion H. induction mb.
    intros. inversion H0. intros. simpl.
    f_equal. apply head_n_app_n. apply H1. apply IHh.
    inversion H. auto. inversion H0. auto. apply H1.
Qed.


Lemma headcolumn_n_n : forall w ma,
  width ma w ->
  headcolumn_n ma w  = ma.
Proof.
  induction w. induction ma. auto.
  intros. simpl. inversion H . apply length_zero_iff_nil in H0.
  rewrite H0. f_equal. apply IHma. auto.
  induction ma. auto. intros. simpl. f_equal.
  apply head_n_tail. apply H. apply IHma. apply H.
Qed.
  
Lemma headcolumn_n_nil_list: forall h w,
  headcolumn_n (nil_list A h) w =dlist_o A Zero h w.
Proof.
  induction h. simpl. auto.
  induction w. simpl. f_equal. apply IHh.
  simpl. f_equal. f_equal. apply head_n_nil.
  apply IHh.
Qed.

Lemma tailcolumn_n_0 : forall ma,
  tailcolumn_n ma 0 = ma.
Proof.
  induction ma. auto. simpl. f_equal. apply IHma.
Qed.

Lemma headcolumn_headcolumn_n: forall w1 ma,
  headcolumn A Zero ma 
  = headcolumn A Zero (headcolumn_n ma (S w1)).
Proof.
  induction w1. induction ma. simpl. auto.
  simpl. f_equal. apply IHma. 
  induction ma. simpl. auto. simpl. f_equal. apply IHma.
Qed.

Lemma headcolumn_n_tailcolumn: forall w1 ma,
  headcolumn_n (tailcolumn A ma) w1 =
  tailcolumn A (headcolumn_n ma (S w1)).
Proof.
  induction w1. induction ma. simpl. auto. 
  intros. simpl. f_equal. apply IHma.
  induction ma. intros. simpl. auto.
  intros. simpl. f_equal. apply IHma.
Qed.

Lemma tailcolumn_n_app: forall w ma mb,
  tailcolumn_n (ma ++mb) w = (tailcolumn_n ma w) ++ (tailcolumn_n mb w).
Proof.
  induction ma.
  induction mb. simpl. auto.
  simpl. f_equal. induction mb. simpl. rewrite ?app_nil_r.
  auto. simpl. f_equal. apply IHma.
Qed. 

Lemma tailcolumn_n_tailcolumn: forall w1 ma,
  tailcolumn_n (tailcolumn A ma) w1 = tailcolumn_n ma (S w1).
Proof.
  induction ma. simpl. auto. simpl. f_equal. apply IHma.
Qed.

Lemma tail_n_nil: forall w,
  tail_n nil w = nil.
Proof.
  induction w. simpl. auto.
  simpl. auto. 
Qed.

Lemma tailcolumn_n_nil_list: forall h w,
  tailcolumn_n (nil_list A h) w = nil_list A h.
Proof.
  induction h. simpl. auto.
  simpl. intros. rewrite tail_n_nil. f_equal.
  apply IHh.
Qed.

Lemma tail_n_app: forall w a b,
  length a = w ->
  tail_n(a++b) w = b.
Proof.
  induction w. - induction a. simpl. auto. intros. inversion H.
  - induction a. intros. inversion H. simpl. intros. apply IHw. inversion H.
    auto.
Qed.

Lemma tailcolumn_n_mlink: forall h w ma mb,
  height ma = h -> height mb = h ->
  width ma  w ->
  tailcolumn_n (mlink A ma mb) w = mb.
Proof.
  induction h.
  - induction w. + induction ma. simpl. intros. rewrite tailcolumn_n_0.
    auto. intros. inversion H. + induction ma. induction mb.
    intros. simpl. auto. intros. inversion H0. intros. inversion H.
  - induction ma. intros. inversion H.
    induction mb. intros. inversion H0. intros. simpl.
    f_equal. apply tail_n_app. apply H1.
    apply IHh. inversion H. auto. inversion H0.
    auto. apply H1.
Qed.
(*
Lemma gettrans_nil_list: forall m n,
  gettrans A Zero (nil_list A m) n = 
  dlist_o A Zero n m.
Proof.
  induction m. simpl. intros. rewrite gettrans_nil.
  rewrite dlist_o_m_0. auto.
  induction n. simpl. auto.
  simpl. f_equal. rewrite headcolumn_nil_list. auto.
  rewrite <- IHn. f_equal. simpl. rewrite tailcolumn_nil_list.
  auto.
Qed. 

Lemma gettrans_app_mlink: forall h1 h2 w ma mb,
  height ma = h1 -> height mb = h2 ->
  width ma w -> width mb w ->
  gettrans A Zero (app ma mb) w =
  mlink' A Zero (gettrans A Zero ma w) 
  (gettrans A Zero mb w) h1.
Proof.
  induction w. simpl. induction h1. simpl. auto. simpl. auto.
  induction ma,h1. simpl. auto. intros. inversion H. intros. inversion H.
  intros. simpl. induction ma. induction a. inversion H1. inversion H3.
  simpl. induction h2,mb. simpl.
*)
Lemma gettrans_app_mlink: forall h1 h2 w ma mb,
  height ma = h1 -> height mb = h2 ->
  width ma w -> width mb w ->
  gettrans A Zero (app ma mb) w =
  mlink A(gettrans A Zero ma w)
  (gettrans A Zero mb w) .
Proof.
  induction h1.
  - intros. apply length_zero_iff_nil in H.
  rewrite H. simpl. rewrite gettrans_nil. rewrite mlink_nil_list_l.
  auto. apply height_gettrans.
  - induction h2.
    + induction w. 
      * intros. simpl. auto.
      * induction ma. intros. inversion H.
        induction mb. intros. simpl. f_equal. rewrite ?app_nil_r.
        auto. rewrite tailcolumn_app . simpl. rewrite app_nil_r.
        rewrite gettrans_nil. rewrite mlink_nil_list_r. auto.
        apply height_gettrans. auto. intros. inversion H0.
    + induction w.  
      * simpl. auto.
      * induction ma. intros. inversion H. induction mb. intros. inversion H0.
        intros. simpl. f_equal. f_equal. apply headcolumn_app.
        rewrite tailcolumn_app. simpl.
        rewrite cons_app. apply IHw. simpl. f_equal. apply height_tailcolumn.
        inversion H. auto. simpl. f_equal. apply height_tailcolumn. inversion H0.
        auto. simpl. split. apply length_tl. apply H1. apply width_tailcolumn.
        apply H1. simpl. split. apply length_tl. apply H2. apply width_tailcolumn.
        apply H2.
Qed.

Lemma gettrans_app: forall w1 w2 ma,
  width ma (w1+w2) -> 
  width (headcolumn_n ma w1) w1 ->
  width (tailcolumn_n ma w1) w2->
  gettrans A Zero ma (w1+w2) 
  = app (gettrans A Zero (headcolumn_n ma w1)w1)
    (gettrans A Zero (tailcolumn_n ma w1) w2).
Proof.
  induction w1. - induction w2.
  * simpl. auto. * intros. simpl. f_equal. rewrite tailcolumn_n_0.
    auto. f_equal. rewrite tailcolumn_n_0. auto.
  - induction w2. intros. * simpl. f_equal.
    rewrite headcolumn_n_n. auto.
    assert(S w1+ 0= S w1). { auto. } rewrite H2 in H. apply H.
    rewrite headcolumn_n_n. rewrite app_nil_r. f_equal. auto.
    assert(S w1+ 0= S w1). { auto. } rewrite H2 in H. apply H. 
    * intros. simpl. f_equal. apply headcolumn_headcolumn_n .
    rewrite IHw1. f_equal. f_equal. apply headcolumn_n_tailcolumn.
    rewrite tailcolumn_n_tailcolumn. simpl. auto. apply width_tailcolumn.
    apply H. apply width_headcolumn_n. apply width_tailcolumn_n.
    apply width_tailcolumn. apply H.
Qed.
  


Lemma headcolumn_n_app: forall h1 h2 w ma mb,
  height ma = h1 -> height mb = h2 ->
  headcolumn_n (ma ++ mb) w = (headcolumn_n ma w)++(headcolumn_n mb w).
Proof.
  induction h1. 
    - induction h2.   
      + induction ma. induction mb. simpl. auto. intros.
        inversion H0. intros. inversion H.
      + induction ma. induction mb. intros. simpl. auto.
        intros. simpl. auto. intros. inversion H.
    - induction h2.
      + induction ma. intros. inversion H. induction mb.
        intros. simpl. f_equal. rewrite ?app_nil_r. auto.
        intros. inversion H0.
      + induction ma. intros. inversion H. induction mb.
        intros. inversion H0. intros. simpl. f_equal.
        apply IHh1 with(h2:=S h2). inversion H. auto.
        apply H0.
Qed.



End column_n.

Section column_nth.

Variable A:Set.
Variable Zero:A.

Fixpoint get_nth (a:list A) i:=
  match i with
  | O => Zero
  | S O => @hd A Zero a
  | S n => get_nth (tl a) n
  end.

Lemma get_nth_nil: forall i,
  get_nth nil i = Zero.
Proof.
  induction i.
  simpl. auto. simpl. rewrite IHi. 
  induction i. auto. auto.
Qed.

Fixpoint column_nth (ma:list(list A)) i:=
  match ma with
  | nil => nil 
  | x::x' => get_nth x i :: column_nth x' i
  end.

Lemma length_column_nth: forall m ma i, 
  length ma = m ->
  length (column_nth ma i) = m.
Proof.
  induction m,ma.
  simpl. auto. intros. inversion H.
  intros. inversion H.
  intros. simpl. auto.
Qed.

Lemma column_nth_nil_list :forall m i,
  column_nth (nil_list A m) i = list_o A Zero m.
Proof.
  induction m.
  simpl. auto.
  simpl. induction i. f_equal.
  auto. f_equal. rewrite get_nth_nil. auto.
  apply IHm. 
Qed.


End column_nth.

Lemma gettrans_compat: forall (A:Set) Zero h w (ma mb: list (list A)),
  height ma = h -> height mb = h ->
  width ma w -> width mb w ->
  ma = mb -> 
  gettrans A Zero ma w = gettrans A Zero mb w.
Proof.
  induction h.
  - induction ma. induction mb. rewrite gettrans_nil. auto.
    intros. inversion H0. intros. inversion H.
  - induction w. simpl. auto.
    + induction ma. intros. inversion H. induction mb.
      intros. inversion H0. intros.
      simpl. f_equal. f_equal. inversion H3. auto.
      inversion H3. auto. apply IHw. simpl.
      f_equal. apply height_tailcolumn. inversion H.
      auto. simpl. f_equal. apply height_tailcolumn.
      inversion H0. auto. simpl. split. apply length_tl.
      apply H1. apply width_tailcolumn. apply H1.
      simpl. split. apply length_tl. apply H2.
      apply width_tailcolumn. apply H2.  inversion H3.
      auto.
Qed.

Lemma trans_compat : 
  forall (A:Set)(Zero:A) m n, 
     forall x x' : (@Mat A m n), @M_eq A m n x x' ->
         @M_eq A n m 
    (trans A Zero x) (trans A Zero x').
Proof.
  induction x,x'. unfold M_eq,trans.
  simpl. intros. apply gettrans_compat with(h:=m). auto.
  auto. auto. auto. auto.
Qed.

Add Parametric Morphism {A:Set}{Zero}{m n :nat}: (trans A Zero)
  with signature (@M_eq A m n) ==> (@M_eq A n m)
  as trans_mor.
Proof.
exact (@trans_compat A Zero m n).
Qed.
